/*
 * HashClauseTest.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include <gtest/gtest.h>

#include "bfr/Literal.hpp"
#include "bfr/Clause.hpp"

namespace bfr { namespace test {

TEST(Clause, insert) {
    Clause *c = new Clause(3);

    Literal *l1 = new Literal(0, false);
    Literal *l2 = new Literal(1, false);
    Literal *l3 = new Literal(2, true);

    Literal *l1Prime = new Literal(1, true);

    Literal *l1Other = new Literal(0, false);
    Literal *l2Other = new Literal(1, false);

    c->add(l1);
    c->add(l2);
    c->add(l3);

    c->add(l1Prime);

    c->add(l1);
    c->add(l2);
    c->add(l3);

    c->add(l1Prime);

    c->add(l1Other);
    c->add(l2Other);

    delete l1Other;
    delete l2Other;

    EXPECT_EQ(4, c->size());
    delete c;
}

TEST(Clause, contains_asString) {
    Clause *c = new Clause(3);

     Literal *l1 = new Literal(0, false);
     Literal *l2 = new Literal(1, false);
     Literal *l3 = new Literal(2, true);

     Literal *l4 = new Literal(0, true);
     Literal *l5 = new Literal(2, false);

     Literal *l6 = new Literal(42, true);
     Literal *l7 = new Literal(100, false);

     c->add(l1);
     EXPECT_EQ("{~x0}", c->asString());
     c->add(l2);
     c->add(l3);

     EXPECT_TRUE(c->contains(l1));
     EXPECT_TRUE(c->contains(l2));
     EXPECT_TRUE(c->contains(l3));

     EXPECT_FALSE(c->contains(l4));
     EXPECT_FALSE(c->contains(l5));
     EXPECT_FALSE(c->contains(l6));
     EXPECT_FALSE(c->contains(l7));
     delete l4;
     delete l5;
     delete l6;
     delete l7;
     delete c;
}

}}
